現状のFormalized Formal Logicで形式化されている事実とされていない事実(様相論理編)
リンク
更新履歴
まえがき
ノーテーション
大体以下の約束をする．
$ FはKripkeフレームとし，断らなければ$ F := \lang W,R\rangとしていつものように定める． $ \Vdashは付値．$ x \in W, p \in \mathrm{Prop}に対して$ x \Vdash pのように書く．
公理$ \varphiがフレームクラス$ Cを規定する：$ C defined by $ \varphiとは，
任意の$ Fに対して$ F \vDash \varphi \iff F \in Cが成り立つこととする．
特に$ Cをフレームになりたつ性質として見るとき，フレームクラスという語を省略する．
例えば「$ \Box p \to pは反射性を規定する」の様に言う．
done: Geach論理についてのKripke健全性およびKripke完全性 $ (i,j,k,m) \in \N^4とする．
Def
Geach公理とは$ \Diamond^i \Box^m p \to \Box^j \Diamond^n pのことを指し，$ \mathsf{ge}_{i,j,k,m}と書く． Def
$ (i,j,k,m)Geach合流性とは$ \forall x,y,z \lbrack x \prec^i y ~\&~ x \prec^j z \implies \exists u \lbrack y \prec^m u ~\&~ z \prec^n u \rbrack \rbrackの事を指す． Thm
Thm